ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A,B:ecl-trans-tuple{i:l}(ds; da),
f:((?)()()), g:().
ecl-trans-normal(A)
 ecl-trans-normal(B)
 (m:. ((f((inr  ),n.ff,n.ff,m))))
 ecl-trans-normal(combine-ecl-tuples2(A; B; f; g)) 

latex

Definitions	t  T, x:A. B(x), b, P  Q, False, A, A  B, , P  Q, P  Q, P  Q, prop{i:l}, , , True, T, Unit, finite-type(T), x. t(x), , no_repeats(T; l), sorted(L), decidable(P), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-trans-normal(x), combine-ecl-tuples2(A; B; f; g), ecl-trans-tuple{i:l}(ds; da), Id, fpf(A; a.B(a)), Knd, ff
Lemmas	bfalse wf, ecl-trans-normal wf, ecl-trans-tuple wf, Knd wf, fpf wf, Id wf, decidable equal product, decidable equal union, decidable equal bool, decidable equal unit, no repeats-merge, sorted-merge, nat plus wf, finite-type-product, finite-type-union, unit wf, finite-type-unit, finite-type-bool, not wf, assert wf, squash wf, true wf, it wf, bool wf, nat wf, eqff to assert, assert of bnot